| 1. Identificação | ||||||||||
| Tipo de Referência | Tese ou Dissertação (Thesis) | |||||||||
| Site | mtc-m21b.sid.inpe.br | |||||||||
| Código do Detentor | isadg {BR SPINPE} ibi 8JMKD3MGPCW/3DT298S | |||||||||
| Identificador | 8JMKD3MGP3W34P/3QLQMU2 | |||||||||
| Repositório | sid.inpe.br/mtc-m21b/2018/03.06.14.06 | |||||||||
| Última Atualização | 2018:05.28.12.30.05 (UTC) simone | |||||||||
| Repositório de Metadados | sid.inpe.br/mtc-m21b/2018/03.06.14.06.09 | |||||||||
| Última Atualização dos Metadados | 2018:06.22.13.21.53 (UTC) simone | |||||||||
| Chave Secundária | INPE-18030-TDI/2740 | |||||||||
| Chave de Citação | Pereira:2018:MoChPr | |||||||||
| Título | Model checking probabilístico para apoiar a mitigação de evento de falta única em Field Programmable Gate Arrays (FPGAs)  | |||||||||
| Título Alternativo | Probabilistic model checking to support the mitigation of single event upset in Field Programmable Gate Arrays (FPGAs) | |||||||||
| Curso | CAP-COMP-SESPG-INPE-MCTIC-GOV-BR | |||||||||
| Ano | 2018 | |||||||||
| Data | 2018-03-28 | |||||||||
| Data de Acesso | 08 maio 2024 | |||||||||
| Tipo da Tese | Dissertação (Mestrado em Computação Aplicada) | |||||||||
| Tipo Secundário | TDI | |||||||||
| Número de Páginas | 134 | |||||||||
| Número de Arquivos | 1 | |||||||||
| Tamanho | 2399 KiB | |||||||||
| 2. Contextualização | ||||||||||
| Autor | Pereira, Viny Cesar | |||||||||
| Banca | Rosa, Reinaldo Roberto (presidente) Santiago Júnior, Valdivino Alexandre de (orientador) Manea, Silvio D'Amore, Roberto | |||||||||
| Endereço de e-Mail | vinycpereira@gmail.com | |||||||||
| Universidade | Instituto Nacional de Pesquisas Espaciais (INPE) | |||||||||
| Cidade | São José dos Campos | |||||||||
| Histórico (UTC) | 2018-03-06 14:07:31 :: viny.pereira@inpe.br -> yolanda.souza@mcti.gov.br :: 2018-04-02 16:54:19 :: yolanda.souza@mcti.gov.br -> viny.pereira@inpe.br :: 2018-05-11 16:07:23 :: viny.pereira@inpe.br -> pubtc@inpe.br :: 2018-05-25 14:58:32 :: pubtc@inpe.br -> administrator :: 2018-05-28 12:23:58 :: administrator -> simone :: 2018-05-28 12:30:06 :: simone :: -> 2018 2018-05-28 12:31:00 :: simone -> administrator :: 2018 2018-06-04 02:28:14 :: administrator -> simone :: 2018 2018-06-22 13:21:53 :: simone -> :: 2018 | |||||||||
| 3. Conteúdo e estrutura | ||||||||||
| É a matriz ou uma cópia? | é a matriz | |||||||||
| Estágio do Conteúdo | concluido | |||||||||
| Transferível | 1 | |||||||||
| Palavras-Chave | verificação formal model checking probabilístico single event upset field programmable gate array formal verification probabilistic model checking | |||||||||
| Resumo | O uso de dispositivos lógicos programáveis como Field Programmable Gate Arrays (FPGAs) em aplicações espaciais cresceu fortemente nos últimos anos devido à sua flexibilidade, custo de desenvolvimento e desempenho. Porém, existe uma exposição excessiva aos raios cósmicos presentes no ambiente e os efeitos da radiação podem causar erros transientes, quando partículas carregadas atingem a superfície dos componentes. Tais efeitos são chamados de Single Event Effects (SEEs), que, em sua forma não destrutiva conhecida como Evento de Falta Única (Single Event Upset (SEU)), pode atingir as células de memória e causar uma inversão no valor lógico armazenado, ou seja, um bit flip. Diversas técnicas de detecção, mitigação e correção de SEU surgiram no passado como forma de evitar falhas, mas a maioria dos testes presentes na literatura foram conduzidos após implementar as técnicas em FPGAs e simular os upsets com ferramentas de injeção de falhas, o que pode ser uma abordagem custosa, já que os resultados só são apresentados ao final das simulações. Por outro lado, modelos estocásticos/probabilísticos podem ser utilizados nos estágios iniciais de um projeto sem a necessidade de implementação, com grande potencial para amortizar o custo do projeto como um todo. Um dos métodos que lida com sistemas de comportamento estocástico é o Model Checking Probabilístico, o qual é capaz de garantir, de acordo com uma probabilidade especificada, a corretude do sistema. Essa dissertação de mestrado investiga a viabilidade, no contexto de aplicações espaciais, da utilização de Model Checking Probabilístico para determinar, dentre um conjunto de soluções, qual seria a melhor técnica de mitigação de SEU em FPGAs SRAM. Para isso, as técnicas de Scrubbing, TMR e código de Hamming foram modeladas via Model Checking Probabilístico com a ferramenta PRISM. Os modelos foram comparados em dois estudos de caso, com características de órbita e tempos de missão distintos, considerando uma Xilinx Virtex-5 em ambos os tipos de ionização, direta e indireta. Considerando três atributos de dependabilidade, disponibilidade, segurança e confiabilidade, as técnicas também foram implementadas e simuladas via ModelSim para obter comparações com os modelos probabilísticos desenvolvidos. As análises dos modelos mostram que, em termos de disponibilidade, o código de Hamming apresentou o melhor desempenho mantendo o sistema por mais tempo em modo operacional mesmo com a pior taxa de falhas. Na confiabilidade, o que mais afetou o Scrubbing foi o tamanho do intervalo entre as correções enquanto a segurança está mais relacionada com a taxa de cobertura. O TMR apresentou os piores resultados pois permite que os upsets se acumulem e deve ser combinado com alguma técnica de correção, como o código de Hamming ou Scrubbing. Já os resultados da comparação com a simulação funcional mostram que as condições de órbita e tempos de missão são fatores impactantes na precisão dos modelos e devem ser considerados. Por fim, é possível confirmar a viabilidade do uso de Model Checking Probabilístico pois, na maioria dos casos, tal abordagem apresentou resultados próximos aos obtidos com simulação funcional. ABSTRACT: The use of programmable logic devices such as Field Programmable Gate Arrays (FPGAs) in space applications has grown strongly in recent years due to its flexibility, development cost and performance. However, there is excessive exposure to the cosmic rays present in the environment and the effects of radiation can cause transient errors, when charged particles reach the surface of the components. These effects are called Single Event Effects (SEEs), which in their non-destructive form known as Single Event Upset (SEU) can reach the memory cells and cause a reversal in the stored logical value, i.e. a bit flip. Several techniques of detection, mitigation and correction of SEU have appeared in the past as a way of avoiding failures, but most of the tests in the literature were conducted after implementing the techniques in FPGAs and simulate upsets with fault injection tools, which can be a costly approach, since the results are only presented at the end of the simulations. On the other hand, stochastic/probabilistic models can be used in the early stages of design without the need of implementation, with great potential to amortize the cost of the design as a whole. One of the methods that deals with stochastic behavior systems is the Probabilistic Model Checking, which is able to guarantee, within a specified probability, the correctness of the system. This masters dissertation investigates the feasibility, in the context of space applications, the use of Probabilistic Model Checking to determine, among a set of solutions, what would be the best SEU mitigation technique in SRAM FPGAs. For this, the Scrubbing, TMR and Hamming code techniques were modeled using Probabilistic Model Checking within the PRISM tool. The models were compared in two case studies, with distinct orbit characteristics and mission times, considering a Xilinx Virtex-5 in both direct and indirect types of ionization. Considering three attributes of dependability, availability, safety and reliability, the techniques were also implemented and simulated via ModelSim to obtain comparisons with the developed probabilistic models. The analyzes of the models show that in terms of availability, the Hamming code presented the best performance by keeping the system longer in operational mode even with the worst failure rate. In reliability, what most affected Scrubbing was the size of the interval between corrections while safety is more related to the coverage rate. TMR showed the worst results because it allows upsets to accumulate and must be combined with some correction technique such as Hamming code or Scrubbing. The results of the comparison with the functional simulation show that the orbit conditions and mission times are impacting factors on the accuracy of models and should be considered. Finally, it is possible to confirm the feasibility of using Probabilistic Model Checking because, in most cases, this approach showed similar results to those obtained with functional simulation. | |||||||||
| Área | COMP | |||||||||
| Arranjo | urlib.net > BDMCI > Fonds > Produção pgr ATUAIS > CAP > Model checking probabilístico... | |||||||||
| Conteúdo da Pasta doc | acessar | |||||||||
| Conteúdo da Pasta source |
| |||||||||
| Conteúdo da Pasta agreement |
| |||||||||
| 4. Condições de acesso e uso | ||||||||||
| URL dos dados | http://urlib.net/ibi/8JMKD3MGP3W34P/3QLQMU2 | |||||||||
| URL dos dados zipados | http://urlib.net/zip/8JMKD3MGP3W34P/3QLQMU2 | |||||||||
| Idioma | pt | |||||||||
| Arquivo Alvo | publicacao.pdf | |||||||||
| Grupo de Usuários | gabinete@inpe.br pubtc@inpe.br viny.pereira@inpe.br yolanda.souza@mcti.gov.br | |||||||||
| Grupo de Leitores | administrator gabinete@inpe.br pubtc@inpe.br viny.pereira@inpe.br yolanda.souza@mcti.gov.br | |||||||||
| Visibilidade | shown | |||||||||
| Licença de Direitos Autorais | urlib.net/www/2012/11.12.15.10 | |||||||||
| Permissão de Leitura | allow from all | |||||||||
| Permissão de Atualização | não transferida | |||||||||
| 5. Fontes relacionadas | ||||||||||
| Repositório Espelho | sid.inpe.br/mtc-m21b/2013/09.26.14.25.22 | |||||||||
| Unidades Imediatamente Superiores | 8JMKD3MGPCW/3F2PHGS | |||||||||
| Lista de Itens Citando | sid.inpe.br/bibdigital/2013/10.12.22.16 1 | |||||||||
| Acervo Hospedeiro | sid.inpe.br/mtc-m21b/2013/09.26.14.25.20 | |||||||||
| 6. Notas | ||||||||||
| Campos Vazios | academicdepartment affiliation archivingpolicy archivist callnumber contenttype copyholder creatorhistory descriptionlevel dissemination doi electronicmailaddress format group isbn issn label lineage mark nextedition notes number orcid parameterlist parentrepositories previousedition previouslowerunit progress resumeid rightsholder schedulinginformation secondarydate secondarymark session shorttitle sponsor subject tertiarymark tertiarytype url versiontype | |||||||||